00100	
00200	
00300	
00400	
00500	
00600	
00700	
00800	
00900	
01000	
01100	
01200	
01300	
01400	
01500	
01600	CS 226 PROJECT
01700	
01800	DOUG LENAT
01900	                MARCH, 1973
02000	
     

00100	
00200	
00300	
00400	
00500	
00600	
00700	
00800	
00900	
01000	INTRODUCTION
01100	
01200	A "sentence" is an axiom, a proposition, or a (properly
01300		quantified) predicate.
01400	
01500	In this brief paper I have sketched how one might 
01600		skirt some of the paradoxes encountered in 
01700		predicate calculus:
01800	
01900	Instead of assuming "every sentence is exclusively either
02000		true or else the negation of that sentence is true"
02100	
02200		We here assume something like "every sentence S is
02300		exclusively either knowable or else it is not knowable,
02400		and if it is knowable then it is exclusively true or
02500		else its negation is (knowable and) true"
02600	
02700	Thus we are able to relegate "bothersome" sentences to this
02800		"no-comment" status.
02900	
03000	note: what I have done here is probably already known
03100		or wrong; but I enjoyed doing it anyway.
     

00100	PART 1: KNOWABILITY, TRUTH
00200	
00300		Sentences are partitioned into two equivalence classes:
00400			knowable  and  unknowable
00500	
00600	k1.	∀π,s,s' . sit(s) ∧ sit(s') ∧ knowable(π,s) ⊃ knowable(π,s')
00700	
00800		that is, knowability is time and situation independent. Here
00900		we use sit(.) as the same kind of situation predicate you
01000		generally use. From this point on, we may as well shorten
01100		∀s.knowable(π,s) , ∃s.knowable(π,s) , knowable(π,s-special)
01200		all to simply knowable(π).
01300	
01400	k2.	∀π,p. knowable(π) ∧ knowwable(p) ⊃
01500		knowable(π ∧ p)  ∧  knowable(¬π)
01600	
01700		that is, all logical combinations of knowable sentences
01800		are knowable.
01900	
02000	k3.	∀π. knowable(π) ≡ true(π)  ∨ true(¬π)
02100		∀π. ¬true(π) ∨ ¬true(¬π)
02200		∀π. true(π) ≡ true(true(π))
02300	k4.	∀π,p. true(π) ∧ true(p) ≡ true(π ∧ p)
02400		∀π,p. true(π) ⊃ true(π ∨ p)
02500	
02600		most of these are merely common-sense characterizations
02700		of truth and faalsity. But note carefully that the first of k3
02800		says that only knowable sentences can be true or false. That is,
02900		we can prove ¬knowable(π) ⊃ ¬true(π) ∧ ¬true(¬π). This may be
03000		dangerous -- or just plain undesirable -- and the remainder of
03100		the paper should be read with a consideration of whether the
03200		≡ in the first line of k3 ought to be merely a ⊃.
03300	
03400	PROPOSITION 1.	∀π,p. true(π) ∧ true(π⊃p) ⊃ true(p)
03500		
03600		this is comforting. the proof is left as an exercise.
03700	
03800	THEOREM 1.	∃π. knowable(π)
03900		proof:
04000			let the statement of the theorem be sentence p.
04100		Then clearly the sentence "true(p) ∨ ¬true(p) ∨ ¬knowable(p)"
04200		is true; hence by k3 it is knowaable; hence there does exist
04300		a knowable sentence.
04400	
04500	COROLLARY 1.	There are an infinite number of knowable sentences.
04600			 (use theorem 1 and k2)
04700	COROLLARY 2.	There are an infinite number of true sentences.
04800			 (use cor. 1 and k3)
04900	COROLLARY 3.	There are an  infinite number of sentences whose
05000			 negations are true. (use cor. 2 and k3)
05100	
     

00100	PART 2: INDIVIDUAL KNOWING, SUREITY AND UNSUREITY
00200	
00300	
00400	Individuals i may know some fact π in some situation s. This is
00500	expressed as k(i,π,s). 
00600	For each individual, for each situation, sentences are partitioned
00700	into those he is sure about and those he is unsure about.
00800	
00900	k6.	∀s,i,π. sit(s) ∧ individual(i) ⊃
01000			S(i,π,s) ≡ k(i,true(π),s) ∨ k(i,true(¬π),s)
01100	
01200		that is, being sure about π means that one knows that π is
01300		true, or else knows that ¬π is true.
01400	
01500	PROPOSITION 2.	∀s,i,π. S(i,π,s) ≡ S(i,¬π,s)
01600		proof: trivial consequence of k6 and the fact that π ≡ ¬¬π
01700	
01800	
01900	Let us characterize formally the notion that situations are linarly
02000	ordered by time. In particular, we assume that no two events occur
02100	at precisely the same instant in time. This last statement is a
02200	consequence of the following axioms, and in fact may be undesirable.
02300	I don't think that this particular aspect of the axioms is ever used.
02400	
02500	k7.	∀s,t. sit(s) ∧sit(t) ≡ later(s,t) ∨ later(t,s)
02600		∀s,t,u. later(s,t) ∧ later(t,u) ⊃ later(s,u)
02700		∀s,t. later(s,t) ∧ later(t,s)  ≡ s=t
02800	k8.	∀i,π,s,t. sit(s) ∧ sit(t) ∧ individual(i) ⊃
02900		  	k(i,π,s) ∧ later(t,s) ⊃ k(i,π,t)
03000	
03100		that is, no one forgets anything once he knows it.
03200	
03300	PROPOSITION 3.	Under the hypotheses of k8, 
03400			S(i,B,s) ∧ later(t,s) ⊃ S(i,B,t)
03500		proof: trivial, using k6 and k8.
03600	
03700	
03800	K9.	∀i,s,π. individual(i) ∧ sit(s) ∧ k(i,true(π),s) ⊃ true(π)
03900	
04000		that is, if i knows π is true, then π must really be true.
04100	
04200	k10.	∀i,s,π. individual(i) ∧ sit(s) ⊃
04300			S(i,π,s) ≡ k(i,true(S(i,π,s)),s)
04400		      ∧ ¬S(i,π,s) ≡ k(i,true(¬S(i,π,s)),s)
04500	
04600		that is, for any sentence p,  an individual i knows whether
04700		or not he is sure about p. Hence each individual knows precisely
04800		which things he is unsure about.
04900	
05000	k11.	∀i,s,p,π. individual(i) ∧ sit(s) ⊃
05100			S(i,π,s) ∧ k(i,true(π≡p),s) ⊃ S(i,p,s)
05200		also    S(i,π,s) ∧ S(i,p,s) ⊃ S(i,π∧p,s)
05300	(k12)   also    S(i,knowable(π),s) ≡ ∃t. sit(t) ∧ S(i,π,t)
05400	
05500		That is, if we're sure that π is knowable, then "it is conceivable
05600		that" (meaning there exists a situation in which) we will someday
05700		know that π is true, or we'll know ¬π is true. Thus we're aware
05800		now of those facts which we may someday know about.
     

00100	PART 2 (continued): LEARNING
00200	
00300	So far, we've left the details of change-of situation alone. Let's
00400	work a bit on this, and extend k12 a little.
00500	
00600	k13.	∀s,π. sit(s) ⊃ sit(learnabout(π,s))
00700		∀π,s,i. sit(s) ∧ individual(i) ∧ S(i,π,s) ⊃
00800			learnabout(π,s)=s
00900		∀π,s,i. sit(s) ∧ individual(i) ∧ knowable(π) ⊃
01000			S(i,π,learnabout(π,s))
01100	
01200		Thus learnabout(π,s) is a function from situations to 
01300		situations; its meaning is "go out into the world and learn
01400		about sentence π if it is possible to do so."
01500	
01600	PROPOSITION 4.	∀i,s,π. sit(s) ∧ individual(i) ⊃ 
01700			S(i,knowable(π),s) ≡ S(i,π,learnabout(π,s))
01800		proof: straightforward, using k12 and k13.
01900	
02000	k14.	∀i,s,π,p. sit(s) ∧ individual(i) ∧ ¬S(i,π,s) 
02100		∧ S(i,π,learnabout(p,s))  ⊃
02200		∃λ. S(i,λ,s) ∧ true((p∧λ)⊃π)
02300	
02400		this just says that if, in learning about p, we also
02500		gain knowledge about some other sentence π, then π must
02600		be implied by p (or by p and other previously-known sentences).
02700	
02800	PROPOSITION 5. ∀s,π,p. learnabout(π,(learnabout(p,s)))
02900			      = learnabout(p,(learnabout(π,s)))
03000	
03100		Thus the order of learning is unimportant.
     

00100	PART 3: THE PRISONER PARADOX
00200	
00300	THEOREM 2.	∃π. ¬knowable(π)
00400		proof:
00500			this is the main result of the paper.
00600			it is proved using the "prisoner paradox"
00700		        We axiomatize the problem and, by assuming
00800			∀π. knowable(π)  we arrive at a contradiction.
00900	
01000	Prisoner p must be hanged in m days or less. He can only be hanged
01100	on day n if he doesn't expect to be hanged that day.
01200	
01300	The paradox arises as follows: p reasons recusively, something
01400	like "I cannot be hanged on day m, for that morning I shall surely
01500	expect to be hanged. Hence I expect not to be hanged on day m.
01600	Hence I must be hanged on day 1 or 2 or...or m-1. But ...(etc)  "
01700	Then, on day m-1, the prisoner is hanged, and he is indeed surprised!!
01800	
01900	The prisoner-problem axioms:
02000	
02100	p1.	∀i. individual(i) ≡ i=p ∨ i=g
02200		MEANING: the only individuals are prisoner p and guard g.
02300	
02400	p2.	∀s. sit(s) ≡ s=day1 ∨ s=day2
02500		MEANING: we assume m in the previous discussion is 2.
02600		
02700	p3.	∀i,s. sit(s) ∧ individual(i) ⊃ k(i,true(∀t.
02800	  		sit(t) ≡ t=day1 ∨ t=day2), s)
02900		MEANING: p and g are always aware of p2.
03000	
03100	p4.	hanging(day1) ≡ ¬hanging(day2)
03200		MEANING: he must be hung on day1 or on day2.
03300	
03400	p5.	∀i,j,s,t. individual(i) ∧ individual(j) ∧ sit(s) ∧ sit(t) ⊃
03500			k(j,true(k,i,true(hanging(day1)≡¬hanging(day2)),s)),t)
03600		MEANING: both p and g are always aware that p4 is true.
03700	
03800	Being surprised is equivalent to being unsure; i.e., to not being sure.
03900	Thus S(i,π,s) essentially means that individual i is NOT surprised by π
04000	in situation s.
04100	
04200	p6.	later(day2,day1)
04300				 [this lets us use k7,k8]
04400	
04500	p7.	S(p,hanging(day1),day2)
04600		MEANING: p knows by day2 whether or not he was hanged on day1.
04700	
04800	p8.	∀i,j. individual(i) ∧ individual(j) ⊃
04900			k(i,true(k(j,true(S(p,hanging(day1),day2)),day1)),day1)
05000		MEANING: both g and p know (on day 1) that
05100				both g and p know (on day 1) that
05200					p7 is true.
05300	p9.	∀s. sit(s)⊃ (hanging(s)⊃ ¬S(p,hanging(s),s))
05400	p10.	∀s,i,j,u. individual(i) ∧ individual(j) ∧ sit(s) ∧ sit(u) ⊃
05500		k(i,true(k(j,true(∀t. sit(t)⊃(hanging(t)⊃¬S(p,hanging(t),t))),s)),u)
05600		MEANING:p cannot be hung if he's sure about it. This fact is known
05700		always by p and g, and each knows that the other knows.
     

00100	PART 3 (continued)
00200	
00300	We now use the formal representation of the prisoner problem,
00400	and some of our previous axioms, to generate a series of lemmas.
00500	Keep in mind that we are assuming that every sentence is true or
00600	else its negation is true --  that is, we are assuming that all
00700	sentences are knowable.
00800	
00900	LEMMA 1. ∀i,j,s,t,u. individual(i) ∧ individual(j) ∧ sit(s) ∧ sit(t)∧sit(u)⊃
01000		k(i,true(k(j,true(S(p,hanging(u),day2)),s)),t)
01100		MEANING: both g and p always know, that both g and p always know
01200		that p is sure (on day2) of whether he is being hung on
01300		day1 or on day2.
01400	
01500	LEMMA 2. under the hyp. of lemma 1,
01600		k(i,true(k(j,true(k(p,true(¬hanging(day2)),day1)),s)),t)
01700		Proof: use p10 and lemma 1
01800	
01900	LEMMA 2B. under same hyp.
02000		k(i,true(k(j,true(k(p,true(hanging(day1)),day1)),s)),t)
02100		Proof: use lemma 2 and p5
02200	
02300	LEMMA 2C. under same hyp.
02400		k(i,true(k(j,true(S(p,hanging(day1),day1)),s)),t)
02500		Proof: use lemma 2B and k6
02600	
02700	LEMMA 2D. under same hyp.
02800		k(i,true(k(j,true(¬hanging(day1)),s)),t)
02900		Proof: use lemma 2C and p10 again
03000	
03100	LEMMA 3A. true(hanging(day1))
03200	LEMMA 3B. true(¬hanging(day1))
03300		Proof: 3A proved directly from Lemma 2B
03400		       3B proved directly from lemma 2D
03500	
03600	This is in direct contradiction with k3.
03700	The trouble is with p10 (and reconciling it with p4)
03800	thus we may suppose that one of these "axioms" is actually not
03900		knowable. In any event, we may be sure that
04000	¬knowable(p1 ∧ p2 ∧ ... ∧ p9 ∧ p10) is true. 
04100	So ∃π.¬knowable(π) and we are done.
04200	
04300	To summmarize the above structure: the proof was based on the simple fact:
04400	∀π.(knowable(π)⊃ true(π) ∧ true(¬π)) ⊃ ¬knowable(π)
04500	This fact is an immediate corollary of k3.
     

00100	
00200	
00300	
00400	
00500	
00600	
00700	
00800	
00900	
01000	
01100	
01200	
01300	
01400	
01500	
01600	
01700	
01800	
01900	
02000	POSTSCRIPT: to J. MCCARTHY:
02100	
02200	
02300	
02400	This is about all that I've done to date along these lines.
02500	I would like to talk with you about such things as:
02600	    related literature
02700	    worthwhileness of continuing along this approach
02800	    percentage of errors and/or nonsense in these pages
02900	    explaining other paradoxes using this system